FDL - Nuprl Lemma : p-co-restrict_wf

Nuprl Lemma : p-co-restrict_wf

A, B:Type, f:(A

(B + Top)), P:(A

), p:(

x:A. Dec(P(x))). p-co-restrict(f;p)

A

(B + Top)

Definitions Type, t T, Top, left + right, x:AB(x), , f(a), x(s), x:A. B(x), Dec(P), x.A(x), x. t(x), p-co-filter(f), f o g , p-co-restrict(f;p)

Lemmas p-compose wf, p-co-filter wf, decidable wf, top wf